Add check for inhabited datatypes #319
Conversation
Uses memoziation but only for provably inhabited No tests yet
joscoh
requested review from
a team,
aqjune-aws,
atomb and
shigoel
as code owners
MikaelMayer
left a comment
MikaelMayer
left a comment
There was a problem hiding this comment.
This PR adds an inhabited type check for datatypes to ensure soundness of destructor generation. The implementation uses memoization to handle mutually recursive types and correctly rejects uninhabited types. The approach is conservative but sound, with excellent test coverage. Minor documentation improvements would be helpful, but the code is solid and ready to merge.
| ) true) | ||
| pure (accC || constrInhab) | ||
| ) false) | ||
| knowType res |
There was a problem hiding this comment.
The termination proof uses Prod.Lex with a tuple (adts.size - seen.length, t.size). While correct, the reasoning could be documented:
| knowType res | |
| knowType res | |
| /-- | |
| Termination: We use lexicographic ordering on (remaining types, type size). | |
| - Left component decreases when we add a type to `seen` | |
| - Right component decreases when we recurse into type arguments | |
| -/ |
| -- A constructor is inhabited if all of its arguments are inhabited | ||
| let constrInhab ← (c.args.foldlM | ||
| (fun accA ty1 => | ||
| do |
There was a problem hiding this comment.
The comment "Only add false if not in a cycle, it may resolve later" is subtle. Consider expanding:
-- Only memoize 'false' if we're not in a cycle (seen.isEmpty).
-- If we're in a cycle, the type might still be inhabited via another path,
-- so we defer memoization until the cycle is fully explored.
if b || seen.isEmpty then
| /-- info: A function of name Int.Add already exists! Redefinitions are not allowed. | ||
| Existing Function: func Int.Add : ((x : int) (y : int)) → int; | ||
| New Function:func Int.Add : ((x : int)) → Bad;-/ | ||
| #guard_msgs in |
There was a problem hiding this comment.
Excellent test coverage
The test additions are comprehensive, covering:
- Standard inhabited types (Option, List, Either, Nat)
- Mutually recursive inhabited types (Even/Odd, Forest/Tree)
- Uninhabited types (Empty, mutually uninhabited cycles)
- Three-way cycles
This is exactly the right level of testing.
Add comments about termination, memoization
2 participants
Issue #, if available: #306
Description of changes:
Adds check to ensure datatypes are inhabited to ensure soundness of destructor generation
This check uses memoization to avoid repeated computation, but is conservative, rejecting types like
List Emptythat are inhabited.By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.